0(#) → #
+(#, x) → x
+(x, #) → x
+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))
+(1(x), 0(y)) → 1(+(x, y))
+(0(x), j(y)) → j(+(x, y))
+(j(x), 0(y)) → j(+(x, y))
+(1(x), 1(y)) → j(+(+(x, y), 1(#)))
+(j(x), j(y)) → 1(+(+(x, y), j(#)))
+(1(x), j(y)) → 0(+(x, y))
+(j(x), 1(y)) → 0(+(x, y))
+(+(x, y), z) → +(x, +(y, z))
opp(#) → #
opp(0(x)) → 0(opp(x))
opp(1(x)) → j(opp(x))
opp(j(x)) → 1(opp(x))
-(x, y) → +(x, opp(y))
*(#, x) → #
*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)
*(j(x), y) → -(0(*(x, y)), y)
*(*(x, y), z) → *(x, *(y, z))
*(+(x, y), z) → +(*(x, z), *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))
↳ QTRS
↳ DependencyPairsProof
0(#) → #
+(#, x) → x
+(x, #) → x
+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))
+(1(x), 0(y)) → 1(+(x, y))
+(0(x), j(y)) → j(+(x, y))
+(j(x), 0(y)) → j(+(x, y))
+(1(x), 1(y)) → j(+(+(x, y), 1(#)))
+(j(x), j(y)) → 1(+(+(x, y), j(#)))
+(1(x), j(y)) → 0(+(x, y))
+(j(x), 1(y)) → 0(+(x, y))
+(+(x, y), z) → +(x, +(y, z))
opp(#) → #
opp(0(x)) → 0(opp(x))
opp(1(x)) → j(opp(x))
opp(j(x)) → 1(opp(x))
-(x, y) → +(x, opp(y))
*(#, x) → #
*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)
*(j(x), y) → -(0(*(x, y)), y)
*(*(x, y), z) → *(x, *(y, z))
*(+(x, y), z) → +(*(x, z), *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))
*1(x, +(y, z)) → *1(x, y)
+1(0(x), 0(y)) → 01(+(x, y))
*1(+(x, y), z) → *1(x, z)
*1(j(x), y) → *1(x, y)
+1(j(x), 0(y)) → +1(x, y)
+1(0(x), j(y)) → +1(x, y)
*1(0(x), y) → 01(*(x, y))
+1(1(x), j(y)) → +1(x, y)
+1(j(x), 1(y)) → +1(x, y)
+1(1(x), 1(y)) → +1(x, y)
OPP(j(x)) → OPP(x)
*1(1(x), y) → +1(0(*(x, y)), y)
+1(j(x), j(y)) → +1(x, y)
*1(x, +(y, z)) → *1(x, z)
*1(1(x), y) → 01(*(x, y))
+1(1(x), 1(y)) → +1(+(x, y), 1(#))
*1(+(x, y), z) → *1(y, z)
-1(x, y) → +1(x, opp(y))
+1(j(x), 1(y)) → 01(+(x, y))
+1(1(x), j(y)) → 01(+(x, y))
*1(0(x), y) → *1(x, y)
OPP(0(x)) → 01(opp(x))
OPP(0(x)) → OPP(x)
+1(+(x, y), z) → +1(y, z)
OPP(1(x)) → OPP(x)
*1(j(x), y) → -1(0(*(x, y)), y)
*1(x, +(y, z)) → +1(*(x, y), *(x, z))
+1(0(x), 0(y)) → +1(x, y)
+1(1(x), 0(y)) → +1(x, y)
+1(0(x), 1(y)) → +1(x, y)
-1(x, y) → OPP(y)
*1(*(x, y), z) → *1(y, z)
*1(+(x, y), z) → +1(*(x, z), *(y, z))
+1(+(x, y), z) → +1(x, +(y, z))
*1(*(x, y), z) → *1(x, *(y, z))
+1(j(x), j(y)) → +1(+(x, y), j(#))
*1(j(x), y) → 01(*(x, y))
*1(1(x), y) → *1(x, y)
0(#) → #
+(#, x) → x
+(x, #) → x
+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))
+(1(x), 0(y)) → 1(+(x, y))
+(0(x), j(y)) → j(+(x, y))
+(j(x), 0(y)) → j(+(x, y))
+(1(x), 1(y)) → j(+(+(x, y), 1(#)))
+(j(x), j(y)) → 1(+(+(x, y), j(#)))
+(1(x), j(y)) → 0(+(x, y))
+(j(x), 1(y)) → 0(+(x, y))
+(+(x, y), z) → +(x, +(y, z))
opp(#) → #
opp(0(x)) → 0(opp(x))
opp(1(x)) → j(opp(x))
opp(j(x)) → 1(opp(x))
-(x, y) → +(x, opp(y))
*(#, x) → #
*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)
*(j(x), y) → -(0(*(x, y)), y)
*(*(x, y), z) → *(x, *(y, z))
*(+(x, y), z) → +(*(x, z), *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
*1(x, +(y, z)) → *1(x, y)
+1(0(x), 0(y)) → 01(+(x, y))
*1(+(x, y), z) → *1(x, z)
*1(j(x), y) → *1(x, y)
+1(j(x), 0(y)) → +1(x, y)
+1(0(x), j(y)) → +1(x, y)
*1(0(x), y) → 01(*(x, y))
+1(1(x), j(y)) → +1(x, y)
+1(j(x), 1(y)) → +1(x, y)
+1(1(x), 1(y)) → +1(x, y)
OPP(j(x)) → OPP(x)
*1(1(x), y) → +1(0(*(x, y)), y)
+1(j(x), j(y)) → +1(x, y)
*1(x, +(y, z)) → *1(x, z)
*1(1(x), y) → 01(*(x, y))
+1(1(x), 1(y)) → +1(+(x, y), 1(#))
*1(+(x, y), z) → *1(y, z)
-1(x, y) → +1(x, opp(y))
+1(j(x), 1(y)) → 01(+(x, y))
+1(1(x), j(y)) → 01(+(x, y))
*1(0(x), y) → *1(x, y)
OPP(0(x)) → 01(opp(x))
OPP(0(x)) → OPP(x)
+1(+(x, y), z) → +1(y, z)
OPP(1(x)) → OPP(x)
*1(j(x), y) → -1(0(*(x, y)), y)
*1(x, +(y, z)) → +1(*(x, y), *(x, z))
+1(0(x), 0(y)) → +1(x, y)
+1(1(x), 0(y)) → +1(x, y)
+1(0(x), 1(y)) → +1(x, y)
-1(x, y) → OPP(y)
*1(*(x, y), z) → *1(y, z)
*1(+(x, y), z) → +1(*(x, z), *(y, z))
+1(+(x, y), z) → +1(x, +(y, z))
*1(*(x, y), z) → *1(x, *(y, z))
+1(j(x), j(y)) → +1(+(x, y), j(#))
*1(j(x), y) → 01(*(x, y))
*1(1(x), y) → *1(x, y)
0(#) → #
+(#, x) → x
+(x, #) → x
+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))
+(1(x), 0(y)) → 1(+(x, y))
+(0(x), j(y)) → j(+(x, y))
+(j(x), 0(y)) → j(+(x, y))
+(1(x), 1(y)) → j(+(+(x, y), 1(#)))
+(j(x), j(y)) → 1(+(+(x, y), j(#)))
+(1(x), j(y)) → 0(+(x, y))
+(j(x), 1(y)) → 0(+(x, y))
+(+(x, y), z) → +(x, +(y, z))
opp(#) → #
opp(0(x)) → 0(opp(x))
opp(1(x)) → j(opp(x))
opp(j(x)) → 1(opp(x))
-(x, y) → +(x, opp(y))
*(#, x) → #
*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)
*(j(x), y) → -(0(*(x, y)), y)
*(*(x, y), z) → *(x, *(y, z))
*(+(x, y), z) → +(*(x, z), *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
OPP(0(x)) → OPP(x)
OPP(j(x)) → OPP(x)
OPP(1(x)) → OPP(x)
0(#) → #
+(#, x) → x
+(x, #) → x
+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))
+(1(x), 0(y)) → 1(+(x, y))
+(0(x), j(y)) → j(+(x, y))
+(j(x), 0(y)) → j(+(x, y))
+(1(x), 1(y)) → j(+(+(x, y), 1(#)))
+(j(x), j(y)) → 1(+(+(x, y), j(#)))
+(1(x), j(y)) → 0(+(x, y))
+(j(x), 1(y)) → 0(+(x, y))
+(+(x, y), z) → +(x, +(y, z))
opp(#) → #
opp(0(x)) → 0(opp(x))
opp(1(x)) → j(opp(x))
opp(j(x)) → 1(opp(x))
-(x, y) → +(x, opp(y))
*(#, x) → #
*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)
*(j(x), y) → -(0(*(x, y)), y)
*(*(x, y), z) → *(x, *(y, z))
*(+(x, y), z) → +(*(x, z), *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
OPP(j(x)) → OPP(x)
OPP(1(x)) → OPP(x)
Used ordering: Polynomial interpretation [25,35]:
OPP(0(x)) → OPP(x)
The value of delta used in the strict ordering is 8.
POL(1(x1)) = 4 + (4)x_1
POL(j(x1)) = 4 + (4)x_1
POL(0(x1)) = x_1
POL(OPP(x1)) = (2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
OPP(0(x)) → OPP(x)
0(#) → #
+(#, x) → x
+(x, #) → x
+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))
+(1(x), 0(y)) → 1(+(x, y))
+(0(x), j(y)) → j(+(x, y))
+(j(x), 0(y)) → j(+(x, y))
+(1(x), 1(y)) → j(+(+(x, y), 1(#)))
+(j(x), j(y)) → 1(+(+(x, y), j(#)))
+(1(x), j(y)) → 0(+(x, y))
+(j(x), 1(y)) → 0(+(x, y))
+(+(x, y), z) → +(x, +(y, z))
opp(#) → #
opp(0(x)) → 0(opp(x))
opp(1(x)) → j(opp(x))
opp(j(x)) → 1(opp(x))
-(x, y) → +(x, opp(y))
*(#, x) → #
*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)
*(j(x), y) → -(0(*(x, y)), y)
*(*(x, y), z) → *(x, *(y, z))
*(+(x, y), z) → +(*(x, z), *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
OPP(0(x)) → OPP(x)
The value of delta used in the strict ordering is 8.
POL(0(x1)) = 4 + (4)x_1
POL(OPP(x1)) = (2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
0(#) → #
+(#, x) → x
+(x, #) → x
+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))
+(1(x), 0(y)) → 1(+(x, y))
+(0(x), j(y)) → j(+(x, y))
+(j(x), 0(y)) → j(+(x, y))
+(1(x), 1(y)) → j(+(+(x, y), 1(#)))
+(j(x), j(y)) → 1(+(+(x, y), j(#)))
+(1(x), j(y)) → 0(+(x, y))
+(j(x), 1(y)) → 0(+(x, y))
+(+(x, y), z) → +(x, +(y, z))
opp(#) → #
opp(0(x)) → 0(opp(x))
opp(1(x)) → j(opp(x))
opp(j(x)) → 1(opp(x))
-(x, y) → +(x, opp(y))
*(#, x) → #
*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)
*(j(x), y) → -(0(*(x, y)), y)
*(*(x, y), z) → *(x, *(y, z))
*(+(x, y), z) → +(*(x, z), *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
+1(0(x), j(y)) → +1(x, y)
+1(j(x), 0(y)) → +1(x, y)
+1(1(x), j(y)) → +1(x, y)
+1(j(x), 1(y)) → +1(x, y)
+1(+(x, y), z) → +1(y, z)
+1(1(x), 1(y)) → +1(x, y)
+1(0(x), 0(y)) → +1(x, y)
+1(0(x), 1(y)) → +1(x, y)
+1(1(x), 0(y)) → +1(x, y)
+1(j(x), j(y)) → +1(x, y)
+1(+(x, y), z) → +1(x, +(y, z))
+1(1(x), 1(y)) → +1(+(x, y), 1(#))
+1(j(x), j(y)) → +1(+(x, y), j(#))
0(#) → #
+(#, x) → x
+(x, #) → x
+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))
+(1(x), 0(y)) → 1(+(x, y))
+(0(x), j(y)) → j(+(x, y))
+(j(x), 0(y)) → j(+(x, y))
+(1(x), 1(y)) → j(+(+(x, y), 1(#)))
+(j(x), j(y)) → 1(+(+(x, y), j(#)))
+(1(x), j(y)) → 0(+(x, y))
+(j(x), 1(y)) → 0(+(x, y))
+(+(x, y), z) → +(x, +(y, z))
opp(#) → #
opp(0(x)) → 0(opp(x))
opp(1(x)) → j(opp(x))
opp(j(x)) → 1(opp(x))
-(x, y) → +(x, opp(y))
*(#, x) → #
*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)
*(j(x), y) → -(0(*(x, y)), y)
*(*(x, y), z) → *(x, *(y, z))
*(+(x, y), z) → +(*(x, z), *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
+1(0(x), j(y)) → +1(x, y)
+1(j(x), 0(y)) → +1(x, y)
+1(1(x), j(y)) → +1(x, y)
+1(j(x), 1(y)) → +1(x, y)
+1(1(x), 1(y)) → +1(x, y)
+1(0(x), 1(y)) → +1(x, y)
+1(1(x), 0(y)) → +1(x, y)
+1(j(x), j(y)) → +1(x, y)
+1(1(x), 1(y)) → +1(+(x, y), 1(#))
+1(j(x), j(y)) → +1(+(x, y), j(#))
Used ordering: Polynomial interpretation [25,35]:
+1(+(x, y), z) → +1(y, z)
+1(0(x), 0(y)) → +1(x, y)
+1(+(x, y), z) → +1(x, +(y, z))
The value of delta used in the strict ordering is 1/8.
POL(1(x1)) = 1/2 + x_1
POL(j(x1)) = 1/2 + x_1
POL(0(x1)) = x_1
POL(+1(x1, x2)) = (1/4)x_1 + (1/4)x_2
POL(+(x1, x2)) = x_1 + x_2
POL(#) = 0
0(#) → #
+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))
+(#, x) → x
+(x, #) → x
+(j(x), 0(y)) → j(+(x, y))
+(1(x), 1(y)) → j(+(+(x, y), 1(#)))
+(1(x), 0(y)) → 1(+(x, y))
+(0(x), j(y)) → j(+(x, y))
+(+(x, y), z) → +(x, +(y, z))
+(j(x), 1(y)) → 0(+(x, y))
+(1(x), j(y)) → 0(+(x, y))
+(j(x), j(y)) → 1(+(+(x, y), j(#)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
+1(0(x), 0(y)) → +1(x, y)
+1(+(x, y), z) → +1(y, z)
+1(+(x, y), z) → +1(x, +(y, z))
0(#) → #
+(#, x) → x
+(x, #) → x
+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))
+(1(x), 0(y)) → 1(+(x, y))
+(0(x), j(y)) → j(+(x, y))
+(j(x), 0(y)) → j(+(x, y))
+(1(x), 1(y)) → j(+(+(x, y), 1(#)))
+(j(x), j(y)) → 1(+(+(x, y), j(#)))
+(1(x), j(y)) → 0(+(x, y))
+(j(x), 1(y)) → 0(+(x, y))
+(+(x, y), z) → +(x, +(y, z))
opp(#) → #
opp(0(x)) → 0(opp(x))
opp(1(x)) → j(opp(x))
opp(j(x)) → 1(opp(x))
-(x, y) → +(x, opp(y))
*(#, x) → #
*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)
*(j(x), y) → -(0(*(x, y)), y)
*(*(x, y), z) → *(x, *(y, z))
*(+(x, y), z) → +(*(x, z), *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
+1(+(x, y), z) → +1(y, z)
+1(+(x, y), z) → +1(x, +(y, z))
Used ordering: Polynomial interpretation [25,35]:
+1(0(x), 0(y)) → +1(x, y)
The value of delta used in the strict ordering is 1/16.
POL(1(x1)) = 0
POL(j(x1)) = 0
POL(0(x1)) = (4)x_1
POL(+1(x1, x2)) = (1/4)x_1
POL(+(x1, x2)) = 1/4 + x_1 + (2)x_2
POL(#) = 0
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
+1(0(x), 0(y)) → +1(x, y)
0(#) → #
+(#, x) → x
+(x, #) → x
+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))
+(1(x), 0(y)) → 1(+(x, y))
+(0(x), j(y)) → j(+(x, y))
+(j(x), 0(y)) → j(+(x, y))
+(1(x), 1(y)) → j(+(+(x, y), 1(#)))
+(j(x), j(y)) → 1(+(+(x, y), j(#)))
+(1(x), j(y)) → 0(+(x, y))
+(j(x), 1(y)) → 0(+(x, y))
+(+(x, y), z) → +(x, +(y, z))
opp(#) → #
opp(0(x)) → 0(opp(x))
opp(1(x)) → j(opp(x))
opp(j(x)) → 1(opp(x))
-(x, y) → +(x, opp(y))
*(#, x) → #
*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)
*(j(x), y) → -(0(*(x, y)), y)
*(*(x, y), z) → *(x, *(y, z))
*(+(x, y), z) → +(*(x, z), *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
+1(0(x), 0(y)) → +1(x, y)
The value of delta used in the strict ordering is 1/4.
POL(0(x1)) = 1/2 + (4)x_1
POL(+1(x1, x2)) = (1/2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
0(#) → #
+(#, x) → x
+(x, #) → x
+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))
+(1(x), 0(y)) → 1(+(x, y))
+(0(x), j(y)) → j(+(x, y))
+(j(x), 0(y)) → j(+(x, y))
+(1(x), 1(y)) → j(+(+(x, y), 1(#)))
+(j(x), j(y)) → 1(+(+(x, y), j(#)))
+(1(x), j(y)) → 0(+(x, y))
+(j(x), 1(y)) → 0(+(x, y))
+(+(x, y), z) → +(x, +(y, z))
opp(#) → #
opp(0(x)) → 0(opp(x))
opp(1(x)) → j(opp(x))
opp(j(x)) → 1(opp(x))
-(x, y) → +(x, opp(y))
*(#, x) → #
*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)
*(j(x), y) → -(0(*(x, y)), y)
*(*(x, y), z) → *(x, *(y, z))
*(+(x, y), z) → +(*(x, z), *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
*1(x, +(y, z)) → *1(x, y)
*1(+(x, y), z) → *1(x, z)
*1(j(x), y) → *1(x, y)
*1(x, +(y, z)) → *1(x, z)
*1(*(x, y), z) → *1(y, z)
*1(*(x, y), z) → *1(x, *(y, z))
*1(+(x, y), z) → *1(y, z)
*1(0(x), y) → *1(x, y)
*1(1(x), y) → *1(x, y)
0(#) → #
+(#, x) → x
+(x, #) → x
+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))
+(1(x), 0(y)) → 1(+(x, y))
+(0(x), j(y)) → j(+(x, y))
+(j(x), 0(y)) → j(+(x, y))
+(1(x), 1(y)) → j(+(+(x, y), 1(#)))
+(j(x), j(y)) → 1(+(+(x, y), j(#)))
+(1(x), j(y)) → 0(+(x, y))
+(j(x), 1(y)) → 0(+(x, y))
+(+(x, y), z) → +(x, +(y, z))
opp(#) → #
opp(0(x)) → 0(opp(x))
opp(1(x)) → j(opp(x))
opp(j(x)) → 1(opp(x))
-(x, y) → +(x, opp(y))
*(#, x) → #
*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)
*(j(x), y) → -(0(*(x, y)), y)
*(*(x, y), z) → *(x, *(y, z))
*(+(x, y), z) → +(*(x, z), *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
*1(+(x, y), z) → *1(x, z)
*1(j(x), y) → *1(x, y)
*1(*(x, y), z) → *1(y, z)
*1(*(x, y), z) → *1(x, *(y, z))
*1(+(x, y), z) → *1(y, z)
*1(0(x), y) → *1(x, y)
*1(1(x), y) → *1(x, y)
Used ordering: Polynomial interpretation [25,35]:
*1(x, +(y, z)) → *1(x, y)
*1(x, +(y, z)) → *1(x, z)
The value of delta used in the strict ordering is 1/16.
POL(1(x1)) = 4 + (4)x_1
POL(j(x1)) = 1/4 + (4)x_1
POL(*1(x1, x2)) = (1/4)x_1
POL(opp(x1)) = 0
POL(-(x1, x2)) = 0
POL(*(x1, x2)) = 4 + (2)x_1 + (4)x_2
POL(0(x1)) = 1/4 + x_1
POL(+(x1, x2)) = 1/4 + (4)x_1 + (4)x_2
POL(#) = 0
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
*1(x, +(y, z)) → *1(x, y)
*1(x, +(y, z)) → *1(x, z)
0(#) → #
+(#, x) → x
+(x, #) → x
+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))
+(1(x), 0(y)) → 1(+(x, y))
+(0(x), j(y)) → j(+(x, y))
+(j(x), 0(y)) → j(+(x, y))
+(1(x), 1(y)) → j(+(+(x, y), 1(#)))
+(j(x), j(y)) → 1(+(+(x, y), j(#)))
+(1(x), j(y)) → 0(+(x, y))
+(j(x), 1(y)) → 0(+(x, y))
+(+(x, y), z) → +(x, +(y, z))
opp(#) → #
opp(0(x)) → 0(opp(x))
opp(1(x)) → j(opp(x))
opp(j(x)) → 1(opp(x))
-(x, y) → +(x, opp(y))
*(#, x) → #
*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)
*(j(x), y) → -(0(*(x, y)), y)
*(*(x, y), z) → *(x, *(y, z))
*(+(x, y), z) → +(*(x, z), *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
*1(x, +(y, z)) → *1(x, y)
*1(x, +(y, z)) → *1(x, z)
The value of delta used in the strict ordering is 1/8.
POL(*1(x1, x2)) = (1/4)x_2
POL(+(x1, x2)) = 1/2 + (4)x_1 + (4)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
0(#) → #
+(#, x) → x
+(x, #) → x
+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))
+(1(x), 0(y)) → 1(+(x, y))
+(0(x), j(y)) → j(+(x, y))
+(j(x), 0(y)) → j(+(x, y))
+(1(x), 1(y)) → j(+(+(x, y), 1(#)))
+(j(x), j(y)) → 1(+(+(x, y), j(#)))
+(1(x), j(y)) → 0(+(x, y))
+(j(x), 1(y)) → 0(+(x, y))
+(+(x, y), z) → +(x, +(y, z))
opp(#) → #
opp(0(x)) → 0(opp(x))
opp(1(x)) → j(opp(x))
opp(j(x)) → 1(opp(x))
-(x, y) → +(x, opp(y))
*(#, x) → #
*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)
*(j(x), y) → -(0(*(x, y)), y)
*(*(x, y), z) → *(x, *(y, z))
*(+(x, y), z) → +(*(x, z), *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))